
#include <string.h>

/*
size_t cli_strtokenize(char *buffer, const char delim, const size_t token_count, const char **tokens)
{
        size_t tokens_found, i;


    for(tokens_found = 0; tokens_found < token_count; ) {
        tokens[tokens_found++] = buffer;
        buffer = strchr(buffer, delim);
        if(buffer) {
            *buffer++ = '\0';
        } else {
            i = tokens_found;
            while(i < token_count)
                tokens[i++] = NULL;

            return tokens_found;
        }
    }
    return tokens_found;
}
*/

int main (int argc, char **argv) {

//size_t cli_strtokenize(char *buffer, const char delim, const size_t token_count, const char **tokens)
//{
    size_t tokens_found, i;
    char *buffer, const char delim, const size_t token_count, const char **tokens;

//start inserted code
    char buffer_val[10];
    const char *tokens_val[10];

    buffer = &buffer_val;
    tokens = &tokens_val;

    klee_make_symbolic(&buffer_val, sizeof(buffer_val), "1");
    klee_make_symbolic(&delim, sizeof(delim), "2");
    klee_make_symbolic(&token_count, sizeof(token_count), "3");
    klee_make_symbolic(&tokens, sizeof(tokens_val), "4");

//end inserted code

    for(tokens_found = 0; tokens_found < token_count; ) {
        tokens[tokens_found++] = buffer;
        buffer = strchr(buffer, delim);
        if(buffer) {
            *buffer++ = '\0';
        } else {
            i = tokens_found;
            while(i < token_count)
                tokens[i++] = NULL;

            return tokens_found;
        }
    }


    return 0;

}
